Inference at * 
Iof proof for Lemma dcdr-to-bool wf:


  P:, d:Dec(P). [d]   

latex

 by (RepUR ``dcdr-to-bool bool decidable`` ( 0)) 
CollapseTHEN (Auto) 

latex

C.

Definitions	Dec(P), , [d], case b of inl(x) => s(x) | inr(y) => t(y), inl x , inr x , , Unit, P  Q, left + right, A, x:A. B(x), t  T, , Type
Lemmas	it wf, unit wf, not wf